In Solving LinkedIn Queens using MiniZinc I wrote about how to solve the LinkedIn Queens problem using MiniZinc, and showed a single example. In Solving LinkedIn Queens with Haskell I saw that there is a large set of instances available, so it's time to benchmark the different MiniZinc solvers.

The benchmarks test several different features, so first it's worth going deeper into what MiniZinc actually is and how it works. In addition, we will talk about how to benchmark solvers and what the different values mean.

Hillel Wayne wrote about solving the LinkedIn Queens problem with SMT in his Computer Things newsletter. This was in turn inspired by Ryan Berger's post Using SAT to Get the World Record on LinkedIn's Queens that solves the same problem using a SAT solver.

Not to be outdone, this post describes how to use MiniZinc to solve the problem in what I think is a more readable and natural expression of the model than either SAT or SMT. As always, YMMV and what is natural and clear to one person is opaque and weird to someone else.